polymorphic lambda-calculus

(Or "second order typed lambda-calculus"). An extension of

typed lambda-calculus allowing functions which take types as

parameters. E.g. the polymorphic function "twice" may be

written:

twice = / t . (f :: t -@# t) . (x :: t) . f (f x)

(where "/" is an upper case Greek lambda and "(v :: T)" is

usually written as v with subscript T). The parameter t will

be bound to the type to which twice is applied, e.g.:

twice Int

takes and returns a function of type Int -@# Int. (Actual type

arguments are often written in square brackets [ ]). Function

twice itself has a higher type:

twice :: Delta t . (t -@# t) -@# (t -@# t)

(where Delta is an upper case Greek delta). Thus /

introduces an object which is a function of a type and Delta

introduces a type which is a function of a type. Polymorphic

lambda-calculus was invented by Jean-Yves Girard in 1971 and

independently by John C. Reynolds in 1974.

(1994-12-16)